﻿/************************************************************************
 * AIDE - Automata Identification Engine
 * Copyright (C) 2012-2013 Ali Khalili (khalili_DOT_ir_@SIGN_gmail_DOT_com)
 * **********************************************************************
 * This program is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License (LGPL) published 
 * by the Free Software Foundation; either version 2.1 of the License, or (at your
 * option) any later version. This program is distributed without any
 * warranty. See the GNU Lesser General Public License for more details. 
 * ***********************************************************************
 * File         :     AIDE\OnlineAlgo\NFMs\L_One.cs
 * Description  :     Implementaion of L_1 algorithm for identification of Deterministic Mealy Machines
 *                    [PhD Thesis by Muhammad Naeem Irfan. See the thesis defence video at: 
 *                    https://mi2s.imag.fr/analysis-and-optimization-of-software-model-inference-algorithms]
 * Change log   :     -28 April 2013:  Development
 *                    -29 April 2013: Optimized "isClosed". Now, we don't check the equality of rows several times!
 *                    [It could be applied for all approaches]
 * To Do        :	  Make it as a child of L_Plus_M -> so we can use the same data structure and functions
 ************************************************************************/
using System;
using System.Collections.Generic;

using AIDE.Base;
using SMLib.Automata.Base;
using SMLib.Automata.MM;
using AIDE.Oracles.NFMs;


namespace AIDE.OnlineAlgo.NFMs
{
    /// <summary>
    /// This is L1 algorithm, an imporoved version of L*M algorithm
    /// [presented in: Analysis and optimization of software model inference algorithms (2012)]
    /// </summary>
    public class L_One: INFM_Learner
    {
        Alphabet inputAlphabet;
        IOracle_MAT_MM myOracle;
        Word lamdaWordC = new Word();

        #region ObservationTable

        List<TD_Row> Sm;
        List<TD_Row_Parrented> Sm_I;
        List<Word> Em;

        #region observation table row
        class TD_Row
        {
            public Word accessString;

            /// <summary>
            /// outputs
            /// </summary>
            public List<Word> Em_Row;

            public int generatedState;

            /// <summary>
            /// Constructor
            /// </summary>
            public TD_Row()
            {
                accessString = new Word();
                Em_Row = new List<Word>();
                generatedState = -1;
            }

            /// <summary>
            /// Copy constructor
            /// </summary>
            /// <param name="r"></param>
            /// <param name="op"></param>
            public TD_Row(TD_Row r, Word op = null)
            {
                generatedState = -1;

                if (op == null)
                    accessString = new Word(r.accessString);
                else
                    accessString = new Word(op);

                Em_Row = new List<Word>();
                for (int i = 0; i < r.Em_Row.Count; i++)
                    Em_Row.Add(r.Em_Row[i]);
            }

            /// <summary>
            /// Assume that the lenght of two rows are the same
            /// </summary>
            /// <param name="anotherRow"></param>
            /// <returns></returns>
            public int FirstDifference(TD_Row t)
            {
                for (int i = 0; i < Em_Row.Count; i++)
                    if (!Em_Row[i].Equals(t.Em_Row[i])) return i;
                return -1;
            }

            /// <summary>
            /// If this row is same as another
            /// </summary>
            /// <param name="anotherRow"></param>
            /// <returns></returns>
            public bool HasSameRow(TD_Row t)
            {
                return FirstDifference(t) == -1;
            }


            public override string ToString()
            {
                string st = "";
                for (int i = 0; i < Em_Row.Count; i++)
                    st += Em_Row[i].ToString();
                return accessString.ToString() + st;
            }
        }

        class TD_Row_Parrented : TD_Row
        {
            public TD_Row parent;
            public TD_Row eqRow;
            public ISymbol lastOutput;

            public TD_Row_Parrented(TD_Row t, Word p = null)
                : base(t, p)
            {
                parent = t;
                lastOutput = null;
                eqRow = null;
            }

            public TD_Row_Parrented()
                : base()
            {
                parent = null;
            }
        }

        #endregion

        /// <summary>
        /// Initialize the observation table
        ///    Let TD be a finite function that maps (SD union SD.Sigma)* ED to {0; 1}
        ///    An observation table (Sm,Em,Tm) can be visualized as a two-dimensional array with rows labeled by the elements of
        ///    SD union SD.Sigma AND columns labeled by the elements of ED, with the entry for a row input in 
        ///    SD union SD.Sigma AND a column e 2 ED equals to TD(input; e).
        /// </summary>
        void InitializeObservationTable()
        {
            //* initialize
            Sm = new List<TD_Row>();
            Sm_I = new List<TD_Row_Parrented>();
            Em = new List<Word>();

            //* 1- Em={}
            //* 2- Sm={""}
            TD_Row r = new TD_Row();
            r.accessString = lamdaWordC;
            Sm.Add(r);

            //3- add all words of Sigma into Sm_I
            foreach (ISymbol symb in inputAlphabet.AllSymbols())
            {
                TD_Row_Parrented r2 = new TD_Row_Parrented();
                //* parent of the new row is R
                r2.parent = r;
                //* and the -empty generated- row is equal to R (obvious)
                r2.eqRow = r;
                r2.accessString.AddSymbol(symb);
                Sm_I.Add(r2);
                LearningLog.LogStartMQ();
                Sm_I[Sm_I.Count - 1].lastOutput = myOracle.OutputTrace(new Word(symb))[0];
                LearningLog.LogFinishMQ();
            }
        }

        /// <summary>
        /// To add another suffix, we need to add a column into the observation table.
        /// This method add the suffix and fill the table
        /// </summary>
        /// <param name="suff">the suffix to be added</param>
        void AddColumn(Word suff)
        {
            Em.Add(suff);
            foreach (TD_Row t1 in Sm)
            {
                LearningLog.LogStartMQ();
                Word myOutput = myOracle.OutputTrace(t1.accessString, suff).Suffix(suff.Length);
                LearningLog.LogFinishMQ();
                t1.Em_Row.Add(myOutput);
            }
            foreach (TD_Row_Parrented t1 in Sm_I)
            {
                LearningLog.LogStartMQ();
                Word myOutput = myOracle.OutputTrace(t1.accessString, suff).Suffix(suff.Length);
                LearningLog.LogFinishMQ();
                t1.Em_Row.Add(myOutput);
                //* check that the row is still equal to the row that was equal or not
                if (t1.eqRow != null && !myOutput.Equals(t1.eqRow.Em_Row[t1.eqRow.Em_Row.Count - 1]))
                {
                    t1.eqRow = null;
                }
            }
        }

        /// <summary>
        /// Check that the observation table is closed myOracle not
        /// </summary>
        /// <returns>
        /// -1: the observation table is Closed
        /// i : the first row number of Sm.Sigma that makes the table un-closed
        /// </returns>
        int isClosed()
        {
            //* alternative optimized implementation;
            for (int i = 0; i < Sm_I.Count; i++)
            {
                if (Sm_I[i].eqRow == null)
                {
                    return i;
                }
            }
            return -1;

            //for (int i = 0; i < Sm_I.Count; i++)
            //{
            //    TD_Row t = Sm_I[i];
            //    bool found = false;
            //    foreach (TD_Row r in Sm)
            //    {
            //        if (r.HasSameRow(t))
            //        {
            //            found = true;
            //            break;
            //        }
            //    }
            //    if (!found) //there is no equivalent row in Sm corresponding to this Sm_I row
            //        return i;
            //}
            //return -1;//the table is closed
        }

        /// <summary>
        /// What is the last output seen by a specific input
        /// </summary>
        /// <param name="w">the input</param>
        /// <returns>the last seen symbol (null if not found)</returns>
        ISymbol LastOutputOf(Word w)
        {
            ISymbol output = null;
            for (int iii = 0; iii < Sm_I.Count; iii++)
            {
                if (w.Equals(Sm_I[iii].accessString))
                {
                    output = Sm_I[iii].lastOutput;
                    return output;
                }
            }

            for (int iii = 0; iii < Sm.Count; iii++)
            {
                if (w.Equals(Sm[iii].accessString))
                {
                    output = ((TD_Row_Parrented)Sm[iii]).lastOutput;
                    return output;
                }
            }
            return null;
        }

        /// <summary>
        /// Build the conjecture automata based on observation table
        /// </summary>
        /// <returns>
        /// the generated automata
        /// </returns>
        MealyMachine BuildConjecture()
        {
            MealyMachine conj = new MealyMachine();
            MealyMachine.Mealy_State currentState, nextState;
            MealyMachine.Mealy_Transition tr;

            int currentRowIndex = 0;
            Word p;
            TD_Row currentRow;

            //* build the initial state
            currentState = new MealyMachine.Mealy_State("0");
            conj.AddState(currentState);
            currentRow = Sm[0];

            //* rows that are converted to state
            List<TD_Row> statedRow = new List<TD_Row>();
            statedRow.Add(Sm[0]);

            //* generate states breast first order
            //* bool anyStateGenerated;
            for (currentRowIndex = 0; currentRowIndex < statedRow.Count; currentRowIndex++)
            {
                currentRow = statedRow[currentRowIndex];
                currentState = (MealyMachine.Mealy_State)conj[currentRowIndex];

                foreach (ISymbol s in inputAlphabet.AllSymbols())
                {
                    p = new Word(currentRow.accessString);
                    p.AddSymbol(s);
                    bool nextRowFound = false;
                    bool stateShoudbeGenerated = true;

                    //find next row (counterexample) in S:
                    for (int i = 1; i < Sm.Count; i++)
                    {
                        if (Sm[i].accessString.Equals(p))
                        {
                            //Found!
                            nextRowFound = true;

                            //find that this row exists in the generated states?
                            for (int j = 0; j < statedRow.Count; j++)
                            {
                                TD_Row r = statedRow[j];
                                if (r.HasSameRow(Sm[i]))
                                {
                                    //* generate transition to this state from current state

                                    //* first: find the output
                                    Word tmp = new Word(currentRow.accessString);
                                    tmp.AddSymbol(s);
                                    ISymbol output = LastOutputOf(tmp);

                                    tr = new MealyMachine.Mealy_Transition(s, output);
                                    tr.SetDestination((MealyMachine.Mealy_State)conj[j]);
                                    currentState.Transitions.Add(tr);
                                    stateShoudbeGenerated = false;
                                    break;
                                }
                            }
                            //if (nextRowFound) break;

                            //a new state shoud be generated!
                            if (stateShoudbeGenerated)
                            {
                                statedRow.Add(Sm[i]);
                                //anyStateGenerated = true;

                                //* first: find the output
                                Word tmp = new Word(currentRow.accessString);
                                tmp.AddSymbol(s);
                                ISymbol output = LastOutputOf(tmp);

                                nextState = new MealyMachine.Mealy_State(conj.Size.ToString());
                                conj.AddState(nextState);
                                tr = new MealyMachine.Mealy_Transition(s, output);

                                tr.SetDestination(nextState);
                                currentState.Transitions.Add(tr);
                            }
                            break;
                        }
                    }
                    if (nextRowFound) continue;

                    //Neg found in Sm? No problem. So find next row (counterexample) in Sm_I:
                    for (int i = 0; i < Sm_I.Count; i++)
                    {
                        if (Sm_I[i].accessString.Equals(p))
                        {
                            stateShoudbeGenerated = true;
                            //find that this row exists in the generated states?
                            for (int j = 0; j < statedRow.Count; j++)
                            {
                                TD_Row r = statedRow[j];
                                if (r.HasSameRow(Sm_I[i]))
                                {
                                    //generate transition to this state from current state

                                    //* first: find the output
                                    Word tmp = new Word(currentRow.accessString);
                                    tmp.AddSymbol(s);
                                    ISymbol output = LastOutputOf(tmp);

                                    tr = new MealyMachine.Mealy_Transition(s, output);
                                    tr.SetDestination((MealyMachine.Mealy_State)conj.GetStates()[j]);
                                    currentState.Transitions.Add(tr);
                                    stateShoudbeGenerated = false;
                                    break;
                                }
                            }
                            if (stateShoudbeGenerated)
                            {
                                //Found in Sm_I! Now, find a row in Sm with similar TD_row
                                for (int k = 1; k < Sm.Count; k++)
                                {
                                    TD_Row r = Sm[k];
                                    if (r.HasSameRow(Sm_I[i]))
                                    {
                                        statedRow.Add(Sm[k]);

                                        //* first: find the output
                                        Word tmp = new Word(currentRow.accessString);
                                        tmp.AddSymbol(s);
                                        ISymbol output = LastOutputOf(tmp);

                                        //anyStateGenerated = true;
                                        nextState = new MealyMachine.Mealy_State(conj.Size.ToString());
                                        conj.AddState(nextState);
                                        tr = new MealyMachine.Mealy_Transition(s, output);
                                        tr.SetDestination(nextState);
                                        currentState.Transitions.Add(tr);
                                        break;
                                    }
                                }
                            }
                            break;
                        }
                    }
                }
            }

            return conj;
        }

        #endregion

        public L_One(IOracle_MAT_MM oracle)
		{
            this.myOracle = oracle;
			this.inputAlphabet = oracle.InputAlphabet;
        }


        /// <summary>
        /// look up for a word in all entries (path) of Sm
        /// </summary>
        /// <param name="lst"></param>
        /// <param name="path"></param>
        /// <returns></returns>
        int indexOfPath(List<TD_Row> lst, Word p)
        {
            for (int i = 0; i < lst.Count; i++)
            {
                if (lst[i].accessString.Equals(p))
                    return i;
            }
            return -1;
        }

        /// <summary>
        /// look up for a word in all entries (path) of Sm_I
        /// </summary>
        /// <param name="lst"></param>
        /// <param name="path"></param>
        /// <returns></returns>
        int indexOfPath(List<TD_Row_Parrented> lst, Word p)
        {
            for (int i = 0; i < lst.Count; i++)
            {
                if (lst[i].accessString.Equals(p))
                    return i;
            }
            return -1;
        }


        MealyMachine conj;

        /// <summary>
        /// This is an optimiezed eq query: if the machine has just one node
        /// </summary>
        /// <param name="conj">the conjecture</param>
        /// <returns>the counterexample</returns>
        Word PerformEqQuery(MealyMachine conj)
        {
            if (conj.Size == 1)
            {
                //* check the cloded ness of table: for size of 2, it is easy!
                for (int i = 0; i < inputAlphabet.Size; i++)
                {
                    for (int j = 0; j < inputAlphabet.Size; j++)
                    {
                        //* input
                        Word w = new Word(inputAlphabet[i], inputAlphabet[j]);

                        //* output
                        LearningLog.LogStartMQ();
                        Word o = myOracle.OutputTrace(w);
                        LearningLog.LogFinishMQ();

                        if (!((MealyMachine.Mealy_State)conj[0]).ListOfAllOutputs(inputAlphabet[j])[0].Equals(o[1]))
                        {
                            //* in fact the table is not closed!
                            return w;
                        }
                    }
                }
            }

            LearningLog.LogStartEQ();
            Word counterex = myOracle.EquivalenceQ(conj);
            LearningLog.LogFinishEQ();

            return counterex;
        }

        /// <summary>
        /// The learning algorithom based on Algorithm.8 (page 87) of the PhD Thesis
        /// </summary>
        /// <returns>The infered Mealy machine</returns>
        public MealyMachine Learn()
        {
            LearningLog.LogStartLearning();

            InitializeObservationTable();
            conj = null;
            while (true)
            {
                //* in the begining, since the table is empty, it would be also closed!
                //* Construct the conjecture
                conj = BuildConjecture();
				conj.InputAlphabet = myOracle.InputAlphabet;

                //* ask for equivalence query
                Word counterexample = PerformEqQuery(conj);

                //* Q: is there any counterexample?
                //* A: No! We found the RIGHT model => return the conjecture!
                if (counterexample == null)
                {
                    LearningLog.LogFinishLearning();
                    return conj;
                }

                bool tableIsClose = true;
                int nc = -1;

                #region Process the counterexample (1by1suffix approach)
                for (int i = 1; i < counterexample.Length; i++)
                {
                    Word suff = counterexample.Suffix(i);
                    if (!Em.Contains(suff))
                    {
                        //* Fill the table for the resulsts of this newly added suffix
                        AddColumn(suff);

                        tableIsClose = true;
                        nc = isClosed();
                        tableIsClose = (nc == -1);
                        if (!tableIsClose) break;
                    }
                }
                #endregion

                #region Make table closed
                while (true)
                {
                    //* remove from Sm.Sigma AND add to Sm
                    TD_Row t = Sm_I[nc];
                    Sm_I.RemoveAt(nc);
                    Sm.Add(t);
                    for (int k = 0; k < Sm_I.Count; k++)
                    {
                        if (Sm_I[k].eqRow == null && Sm_I[k].HasSameRow(t))
                        {
                            Sm_I[k].eqRow = t;
                        }
                    }

                    //* add anotherRow.a for each a in Sigma if they are not exist there
                    foreach (ISymbol a in inputAlphabet.AllSymbols())
                    {
                        TD_Row_Parrented nt = new TD_Row_Parrented(t);
                        nt.accessString.AddSymbol(a);

                        //* set "last output"
                        LearningLog.LogStartMQ();
                        Word lo = myOracle.OutputTrace(nt.accessString);
                        LearningLog.LogFinishMQ();

                        nt.lastOutput = lo[lo.Length - 1];

                        //don't add anotherRow if there is already one
                        if (indexOfPath(Sm_I, nt.accessString) > -1)
                            continue;

                        Sm_I.Add(nt);
                        for (int k = 0; k < t.Em_Row.Count; k++)
                        {
                            LearningLog.LogStartMQ();
                            Word output = myOracle.OutputTrace(nt.accessString, Em[k]);
                            LearningLog.LogFinishMQ();

                            nt.Em_Row[k] = output.Suffix(Em[k].Length);
                        }

                        for (int k = 0; k < Sm.Count; k++)
                        {
                            if (nt.HasSameRow(Sm[k]))
                            {
                                nt.eqRow = Sm[k];
                                break;
                            }
                        }
                    }

                    nc = isClosed();
                    tableIsClose = (nc == -1);
                    if (tableIsClose) break;
                }
                #endregion
            }
        }
    }
}
